typedef int v4si __attribute__((vector_size(16)));

int i = 2;
int main(int argc, char **argv) {
  v4si v = {0, 1, 2, 3};
  v[i] = 42;
  printf("%d\n", v[2]);
  return 0;
}